\begin{tabbing}
$\forall$\=${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $P$, $Q$:(\{$e$:E$\mid$ loc($e$) = source($l$) $\in$ Id\} $\rightarrow\mathbb{P}$), $B$:Type,\+
\\[0ex]${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(\{$e$:E$\mid$ loc($e$) = source($l$) $\in$ Id\} $\rightarrow$$B$).
\-\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) = source($l$) $\in$ Id\} . $P$($e$) $\Leftarrow\!\Rightarrow$ $Q$($e$))
\\[0ex]$\Rightarrow$ \=(es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$P$($e$);$e$.$f$($e$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$Q$($e$);$e$.$f$($e$)))
\-
\end{tabbing}